$\forall$$A$:Type, $B$:($A$$\rightarrow$Type), $p$:($a$:$A$ $\times$ $B$($a$)). $<$$p$.1, $p$.2$>$ = $p$